package org.eclipse.iota.rules;

import java.util.HashSet;
import java.util.Set;

import org.eclipse.iota.bounds.OldIotaBoundCalculator;
import org.eclipse.iota.model.Boolean;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Inclusion;
import org.eclipse.iota.model.Parameter;
import org.eclipse.iota.model.Property;
import org.eclipse.iota.model.Reference;
import org.eclipse.iota.model.Variable;
import org.eclipse.iota.rewrite.AbstractIotaRule;
import org.eclipse.iota.util.IotaComparisonUtil;

/**
 * @author Christian Krause
 * @generated NOT
 */
public class InfiniteDescent extends AbstractIotaRule {
	
	@Override
	public boolean apply(Inclusion inclusion, boolean change) {
		
		// Must be a recursion.
		if (!inclusion.isRecursion()) {
			return false;
		}
		Property property = (Property) inclusion.getClause().getAlternation().getDefinition();

		// Get the clause.
		Clause clause = inclusion.getClause();

		// Check if all parameters have a lower bound.
		for (Parameter param : property.getParameters()) {
			if (OldIotaBoundCalculator.calculateLowerBound(new Reference(param), clause)==null) {
				return false;
			}
		}
		
		Set<Parameter> matched = new HashSet<Parameter>();
		boolean smaller = false;
		
		// Test all arguments.
		for (Variable argument : inclusion.getArguments()) {
			
			// Must not be matched already.
			if (matched.contains(argument)) {
				return false;
			}
			
			if (argument instanceof Parameter) {
				matched.add((Parameter) argument);
			} else {
				// An existential.
				Reference ref = new Reference(argument);
				for (Parameter parameter : property.getParameters()) {
					if (!matched.contains(parameter) &&
						IotaComparisonUtil.isLessThan(ref, new Reference(parameter), clause)) {
						matched.add(parameter);
						smaller = true;
					}
				}
			}			
		}
		
		// Check if all parameters where matched and at least one is smaller.
		if (smaller && matched.containsAll(property.getParameters())) {
			
			// So it is an infinite descent.
			if (change) {
				clause.getConstraints().clear();
				clause.getConstraints().add(new Boolean(false));
				clause.getExistentials().clear();
			}
			return true;
		}
		
		return true;
		
	}
	
	/*
	 * (non-Javadoc)
	 * @see org.eclipse.iota.rules.AbstractIotaRule#getPriority()
	 */
	@Override
	public int getPriority() {
		return PRIORITY_VERY_HIGH;
	}
	
}
